#|
conway-topo: An ACL2 implementation of Conway's Game of Life on several topologies
Copyright (C) 2007 Vanessa Cheney, Jennifer Foley, Gerardo Gonzalez and John O'Hare

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
|#
;;===== Environment setup ======================================================

  (in-package "ACL2")
  (set-compile-fns t)
  (set-state-ok t)
  (include-book "data-structures/structures" :dir :system)
  (include-book "world" :dir :teachpacks)
   ;;==============================================================================


#| 
This is the insertion of the modified AVL book by Dr. Page. 
Modifications were made to allow pairs to be inserted into tree
|#
;;___________________________________________________________________________________
;;=======  Module: AVL trees   ================================================
;; Defining
;;   (avl-retrieve tr key)
;;   (empty-tree)
;;   (avl-insert tr key datum)
;;   (avl-delete tr key)
;;   (avl-flatten tr)
;;=============================================================================
;; Module usage notes
;;
;; Place this file in the following directory
;;    C:/ACL2-3.1/acl2-sources/books/SE/
;;
;;  Use the following command to certify the module
;;  (certify-book "C:/ACL2-3.1/acl2-sources/books/SE/avl-rational-keys")
;;
;; Command to get access to module functions (any session or program)
;;  (include-book "SE/avl-rational-keys" :dir :system)
;;
;;=============================================================================
;; Function usage notes
;;
;; 1. (avl-retrieve tr key)
;;   assumes
;;     tr         has been constructed by one of the AVL-tree constructors
;;                (empty-tree, avl-insert, and avl-delete)
;;     new-key    is a rational number
;; 
;;   delivers
;;     either a two element list (k d)
;;       such that k equals key and
;;                 tr contains a subtree with k and d in its root
;;     or nil, in case key does not occur in tr
;;   
;; 2. (empty-tree)
;;   delivers an empty AVL-tree
;;
;; 3. (avl-insert tr key datum)
;;   assumes
;;      tr       has been constructed by the AVL-tree constructors
;;               (empty-tree, avl-insert, or avl-delete)
;;      key      is a rational number
;;   delivers an AVL tree with the following property
;;     (and (equal (avl-retrieve (avl-insert tr key datum) key)
;;                 (list key datum))
;;          (iff (avl-retrieve (avl-insert tr key datum) k)
;;               (or (avl-retrieve tr k)
;;                   (key= k key))))
;;
;; 4. (avl-delete tr key)
;;   assumes
;;      tr       has been constructed by the AVL-tree constructors
;;               (empty-tree, avl-insert, and avl-delete)
;;      key      is a rational number
;;   delivers an AVL tree with the following property
;;     (equal (avl-retrieve (avl-delete tr key) key)
;;            nil)
;;
;; 5. (avl-flatten tr)
;;   assumes
;;      tr       has been constructed by the AVL-tree constructors
;;               (empty-tree, avl-insert, and avl-delete)
;;   delivers a list of cons-pairs with the following properties
;;      (and (implies (occurs-in-tree? k tr)
;;                    (and (occurs-in-pairs? k (avl-flatten tr))
;;                         (meta-property-DF tr k)))
;;           (implies (not (occurs-in-tree? k tr))
;;                    (not (occurs-in-pairs? k (avl-flatten tr)))))
;;           (increasing-pairs? (avl-flatten tr)))
;;     where (meta-property-DF tr k) means that one of the elements, e, in
;;     the list (avl-flatten tr) satisfies (equal (car e) k)) and
;;     (cadr e) is the datum at the root of the subtree of tr where k occurs
;;
;;=============================================================================


 ;Used for the height and width of the GUI display window

  (defconst *WIDTH*  1000)
  (defconst *HEIGHT* 1000)
  (defconst *REGULAR* 0)
  
; Coord functions
(defun Coord (x y)
  (cons x y))

(defun isCoord (c)
  (and (consp c)
       (integerp (car c))
       (integerp (cdr c))))

(defun Coord-cellX (c) 
  (car c))

(defun Coord-cellY (c) 
  (cdr c))

; Extractors (and empty-tree detector)
(defun empty-tree? (tr) (not (consp tr)))

(defun height (tr) (if (empty-tree? tr) 0 (car tr)))

(defun key (tr) (cadr tr))

(defun data (tr) (caddr tr))

(defun left (tr) (cadddr tr))

(defun right (tr) (car (cddddr tr)))

(defun keys (tr)
  (if (empty-tree? tr)
      nil
      (append (keys (left tr)) (list (key tr)) (keys (right tr)))))

; Constructors
(defun empty-tree ( ) nil)

(defun tree (k d lf rt)
		(list (+ 1 (max (height lf) (height rt))) k d lf rt))

; Contstraint detectors and key comparators
(defun key? (k) (isCoord k))      ; to change representation of keys

(defun key< (j k) 
  (if (< (car j) (car k))
      t
      (if (= (car j) (car k))
          (< (cdr j) (cdr k))
	  nil)))                  ;     alter definitions of key? and key<

(defun key> (j k) (key< k j))

(defun key= (j k)		  ; note: definitions of
  (and (not (key< j k))           ;    key>, key=, and key-member	
       (not (key> j k))))	  ;        get in line automatically

(defun key-member (k ks)
  (and (consp ks)
       (or (key= k (car ks))
           (key-member k (cdr ks)))))

(defun data? (d)
  (if d t t))

(defun tree? (tr)
  (or (empty-tree? tr)
      (and (natp (height tr))		       ; height
           (= (height tr)                      ;   constraints
              (+ 1 (max (height (left tr))
                        (height (right tr)))))
           (key? (key tr))                     ; key constraint
           (data? (data tr))                   ; data constraint
           (tree? (left tr))                   ; subtree
           (tree? (right tr)))))               ;   constraints


; Key occurs in tree detector
(defun occurs-in-tree? (k tr)
  (and (key? k)
       (tree? tr)
       (key-member k (keys tr))))

;(defun alternate-occurs-in-tree? (k tr)
;  (and (key? k)
;       (tree? tr)
;       (not (empty-tree? tr))
;       (or (key= k (key tr))
;           (alternate-occurs-in-tree? k (left tr))
;           (alternate-occurs-in-tree? k (right tr)))))

; all-key comparators
(defun all-keys< (k ks)
  (or (not (consp ks))
      (and (key< (car ks) k) (all-keys< k (cdr ks)))))

(defun all-keys> (k ks)
  (or (not (consp ks))
      (and (key> (car ks) k) (all-keys> k (cdr ks)))))

; definitions of ordered and balanced, and avl-tree detector
(defun ordered? (tr)
  (or (empty-tree? tr)
      (and (tree? tr)
           (all-keys< (key tr) (keys (left tr)))
           (all-keys> (key tr) (keys (right tr)))
           (ordered? (left tr))
           (ordered? (right tr)))))

(defun balanced? (tr)
  (and (tree? tr)
       (or (empty-tree? tr)
           (and (<= (abs (- (height (left tr)) (height (right tr)))) 1)
           (balanced? (left tr))
           (balanced? (right tr))))))

(defun avl-tree? (tr)
  (and (ordered? tr)
       (balanced? tr)))

; rotations
(defun easy-R (tr)
  (let* ((z (key tr)) (dz (data tr))
         (zL (left tr)) (zR (right tr))
         (x (key zL)) (dx (data zL))
         (xL (left zL)) (xR (right zL)))
     (tree x dx xL (tree z dz xR zR))))

(defun easy-L (tr)
  (let* ((z (key tr)) (dz (data tr))
         (zL (left tr)) (zR (right tr))
         (x (key zR)) (dx (data zR))
         (xL (left zR)) (xR (right zR)))
     (tree x dx (tree z dz zL xL) xR)))

(defun left-heavy? (tr)
  (and (tree? tr)
       (not (empty-tree? tr))
       (= (height (left tr)) (+ 2 (height (right tr))))))

(defun outside-left-heavy? (tr)
  (and (left-heavy? tr)
       (or (= (height (left (left tr)))
              (height (right (left tr))))
           (= (height (left (left tr)))
              (+ 1 (height (right (left tr))))))))

(defun right-rotatable? (tr)
  (and (ordered? tr)
       (not (empty-tree? tr))
       (balanced? (left tr))
       (balanced? (right tr))
       (not (empty-tree? (left tr)))))

(defun right-heavy? (tr)
  (and (tree? tr)
       (not (empty-tree? tr))
       (= (height (right tr)) (+ 2 (height (left tr))))))

(defun outside-right-heavy? (tr)
  (and (right-heavy? tr)
       (or (= (height (right (right tr))) (height (left (right tr))))
           (= (height (right (right tr))) (+ 1 (height (left (right tr))))))))

(defun left-rotatable? (tr)
  (and (tree? tr)
       (not (empty-tree? tr))
       (balanced? (left tr))
       (balanced? (right tr))
       (not (empty-tree? (right tr)))))

(defun hard-R (tr)
  (let* ((z (key tr))
         (dz (data tr))
         (zL (left tr))
         (zR (right tr)))
     (easy-R (tree z dz (easy-L zL) zR))))

(defun hard-L (tr)
  (let* ((z (key tr))
         (dz (data tr))
         (zL (left tr))
         (zR (right tr)))
     (easy-L (tree z dz zL (easy-R zR)))))

(defun inside-left-heavy? (tr)
  (and (left-heavy? tr)
       (= (height (right (left tr)))
          (+ 1 (height (left (left tr)))))))

(defun hard-R-rotatable? (tr)
  (and (right-rotatable? tr)
       (left-rotatable? (left tr))))

(defun inside-right-heavy? (tr)
  (and (right-heavy? tr)
       (= (height (left (right tr)))
          (+ 1 (height (right (right tr)))))))

(defun hard-L-rotatable? (tr)
  (and (left-rotatable? tr)
       (right-rotatable? (right tr))))

(defun rot-R (tr)
  (let ((zL (left tr)))
     (if (< (height (left zL)) (height (right zL)))
         (hard-R tr)
         (easy-R tr))))

(defun rot-L (tr)
  (let ((zR (right tr)))
     (if (< (height (right zR)) (height (left zR)))
         (hard-L tr)
         (easy-L tr))))

; insertion
(defun avl-insert (tr new-key new-datum)
  (if (empty-tree? tr)
      (tree new-key new-datum (empty-tree) (empty-tree))
      (if (key< new-key (key tr))
          (let* ((subL (avl-insert (left tr) new-key new-datum))
                 (subR (right tr))
                 (new-tr (tree (key tr) (data tr) subL subR)))
             (if (= (height subL) (+ (height subR) 2))
                 (rot-R new-tr)
                        new-tr))
          (if (key> new-key (key tr))
              (let* ((subL (left tr))
                     (subR (avl-insert (right tr) new-key new-datum))
                     (new-tr (tree (key tr) (data tr) subL subR)))
                 (if (= (height subR) (+ (height subL) 2))
                     (rot-L new-tr)
                     new-tr))
              (tree new-key new-datum (left tr) (right tr))))))

; delete root - easy case
(defun easy-delete (tr)
  (right tr))

; tree shrinking
(defun shrink (tr)
  (if (empty-tree? (right tr))
      (list (key tr) (data tr) (left tr))
      (let* ((key-data-tree (shrink (right tr)))
             (k (car key-data-tree))
             (d (cadr key-data-tree))
             (subL (left tr))
             (subR (caddr key-data-tree))
             (shrunken-tr (tree (key tr) (data tr) subL subR)))
         (if (= (height subL) (+ 2 (height subR)))
             (list k d (rot-R shrunken-tr))
             (list k d shrunken-tr)))))

(defun raise-sacrum (tr)
   (let* ((key-data-tree (shrink (left tr)))
          (k (car key-data-tree))
          (d (cadr key-data-tree))
          (subL (caddr key-data-tree))
          (subR (right tr))
          (new-tr (tree k d subL subR)))
     (if (= (height subR) (+ 2 (height subL)))
         (rot-L new-tr)
         new-tr)))

; delete root - hard case
(defun delete-root (tr)
  (if (empty-tree? (left tr))
      (easy-delete tr)
      (raise-sacrum tr)))

; deletion
(defun avl-delete (tr k)
  (if (empty-tree? tr)
      tr
      (if (key< k (key tr))           ; key occurs in left subtree
          (let* ((new-left (avl-delete (left tr) k))
                 (new-tr (tree (key tr) (data tr) new-left (right tr))))
             (if (= (height (right new-tr)) (+ 2 (height (left new-tr))))
                 (rot-L new-tr)
                 new-tr))
          (if (key> k (key tr))       ; key occurs in right subtree
              (let* ((new-right (avl-delete (right tr) k))
                     (new-tr (tree (key tr) (data tr) (left tr) new-right)))
                     (if (= (height (left new-tr)) (+ 2 (height (right new-tr))))
                         (rot-R new-tr)
                         new-tr))
                 (delete-root tr)))))  ; key occurs at root

; retrieval
(defun avl-retrieve (tr k)  ; delivers key/data pair with key = k
  (if (empty-tree? tr)      ; or nil if k does not occur in tr
      nil                                 ; signal k not present in tree
      (if (key< k (key tr))
          (avl-retrieve (left tr) k)      ; search left subtree
          (if (key> k (key tr))
              (avl-retrieve (right tr) k) ; search right subtree
              (cons k (data tr))))))      ; k is at root, deliver key/data pair

(defun avl-flatten (tr)  ; delivers all key/data cons-pairs
  (if (empty-tree? tr)   ; with keys in increasing order
      nil
      (append (avl-flatten (left tr))
              (list (cons (key tr) (data tr)))
              (avl-flatten (right tr)))))

(defun occurs-in-pairs? (k pairs)
  (and (consp pairs)
       (or (key= k (caar pairs))
           (occurs-in-pairs? k (cdr pairs)))))

(defun increasing-pairs? (pairs)
  (or (not (consp (cdr pairs)))
      (and (key< (caar pairs) (caadr pairs))
           (increasing-pairs? (cdr pairs)))))

;;_______________ End of AVL code _______________________________________________

#|this function tkats the output of flatten-tree and puts it
in the right format|#
(defun flatTree (list)
  (if (listp list)
      (if (not(null list))
          (cons (car(car list)) (flatTree (cdr list)))
          nil)
      nil))

(defun isAlive (cell tree)
  (if (key-member cell (flatTree (avl-flatten tree)))
      t
      nil))

#|
Removes duplicates from a given sorted list

@param list A sorted true list of rational numbers
@return The same list, but with duplicate entries removed
|#
(defun removeDupsHelper (list nlist)
  (if (listp list)
      (if (not(null list))
          (if (key-member (car list) nlist)
              (removeDupsHelper (cdr list) nlist)
              (removeDupsHelper (cdr list) (cons (car list) nlist)))
          nlist)
      nil))
                    
(defun removeDups (list)
  (if (listp list)
      (removeDupsHelper list nil)
      nil))




#|
Gives the adjacent neighbor of a cell positioned north
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param cell coodinate structure of the cell from which we 
want to get the neighbor
@param w width of the grid
@param h height of the grid
@return the cell at the requested position
|#

(defun aboveNeighbor (topology cell h)
  (if (and (equal (Coord-cellY cell) 0)
          (not (equal topology 'infiniteHex!)))
      (cond ((equal topology 'cylinder) (Coord (Coord-cellX cell) (- h 1)))
            ((equal topology 'torus) (Coord (Coord-cellX cell) (- h 1)))
            ((equal topology 'mobius)(Coord (- (- h 1) (Coord-cellX cell)) (- h 1) ))
            ((equal topology 'klein) (Coord (- (- h 1) (Coord-cellX cell)) (- h 1) ))
            (t cell))
      (Coord (Coord-cellX cell)  (- (Coord-cellY cell) 1) )))

#|
Gives the adjacent neighbor of a cell positioned south
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param cell coodinate structure of the cell from which we 
want to get the neighbor
@param w width of the grid
@param h height of the grid
@return the cell at the requested position
|#
(defun belowNeighbor (topology cell h)
  (if (and (= (Coord-cellY cell) (- h 1))
           (not (equal topology 'infiniteHex!)))
      (cond ((equal topology 'cylinder) (Coord (Coord-cellX cell) 0))
            ((equal topology 'torus) (Coord (Coord-cellX cell) 0))
            ((equal topology 'mobius)(Coord (- (- h 1) (Coord-cellX cell)) 0 ))
            ((equal topology 'klein) (Coord (- (- h 1) (Coord-cellX cell)) 0 ))
            (t cell))
      (Coord (Coord-cellX cell) (+ (Coord-cellY cell) 1) )))

#|
Gives the adjacent neighbor of a cell positioned west
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param cell coodinate structure of the cell from which we 
want to get the neighbor
@param w width of the grid
@param h height of the grid
@return the cell at the requested position
|#
(defun leftNeighbor (topology cell w)
  (if (and (= (Coord-cellX cell) 0)
           (not (equal topology 'infiniteHex!)))
      (cond ((equal topology 'torus) (Coord (- w 1) (Coord-cellY cell)))
            ((equal topology 'klein) (Coord (- w 1) (- (- w 1) (Coord-cellY cell))))
            (t cell))      
      (Coord  (- (Coord-cellX cell) 1) (Coord-cellY cell))))

#|
Gives the adjacent neighbor of a cell positioned east
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param cell coodinate structure of the cell from which we 
want to get the neighbor
@param w width of the grid
@param h height of the grid
@return the cell at the requested position
|#
(defun rightNeighbor (topology cell w)
  (if (and (= (Coord-cellX cell) (- w 1))
           (not (equal topology 'infiniteHex!)))
      (cond ((equal topology 'torus) (Coord 0 (Coord-cellY cell)))
            ((equal topology 'klein) (Coord 0 (- (- w 1) (Coord-cellY cell))))
            (t cell)) 
      (Coord (+ (Coord-cellX cell) 1) (Coord-cellY cell) )))

#|
Gives the adjacent neighbor of a cell positioned north-west
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param cell coodinate structure of the cell from which we 
want to get the neighbor
@param w width of the grid
@param h height of the grid
@return the cell at the requested position
|#
(defun aboveLeftNeighbor (topology cell w h)
  (let* ((c (aboveNeighbor topology cell h)))
    (leftNeighbor topology c w)))
#|
Gives the adjacent neighbor of a cell positioned north-east
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param cell coodinate structure of the cell from which we 
want to get the neighbor
@param w width of the grid
@param h height of the grid
@return the cell at the requested position
|#      
(defun aboveRightNeighbor (topology cell w h)
  (let* ((c (aboveNeighbor topology cell h)))
    (rightNeighbor topology c w)))

#|
Gives the adjacent neighbor of a cell positioned north-west
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param cell coodinate structure of the cell from which we 
want to get the neighbor
@param w width of the grid
@param h height of the grid
@return the cell at the requested position
|#
(defun belowLeftNeighbor (topology cell w h)
  (let* ((c (belowNeighbor topology cell h)))
    (leftNeighbor topology c w)))

#|
Gives the adjacent neighbor of a cell positioned north-east
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param cell coodinate structure of the cell from which we 
want to get the neighbor
@param w width of the grid
@param h height of the grid
@return the cell at the requested position
|#
(defun belowRightNeighbor (topology cell w h)
  (let* ((c (belowNeighbor topology cell h)))
    (rightNeighbor topology c w)))

(defun removeNils (xs)
  (if (> (len xs) 0)
      (if (equal nil (car xs))
          (removeNils (cdr xs))
          (cons (car xs) (removeNils (cdr xs))))
      nil))

#| 
Give all the neighbors surrounding a cell in the grid
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param cell coodinate structure of the cell from which we 
want to get the neighbor
@param w width of the grid
@param h height of the grid
@return A list of all the cells surrounding the given cell
|#
(defun getNeighbors (topology cell w h)
  (if (equal topology 'infiniteHex!)
      (removeNils
       (list
        (aboveNeighbor topology cell h)
        (belowNeighbor topology cell h)
        (leftNeighbor topology cell w)
        (rightNeighbor topology cell w)
        (aboveLeftNeighbor topology cell w h)
        (aboveRightNeighbor topology cell w h) nil))
  (removeNils
   (list
    (aboveNeighbor topology cell h)
    (belowNeighbor topology cell h)
    (leftNeighbor topology cell w)
    (rightNeighbor topology cell w)
    (belowLeftNeighbor topology cell w h)
    (belowRightNeighbor topology cell w h)
    (aboveLeftNeighbor topology cell w h)
    (aboveRightNeighbor topology cell w h) nil))))

#|
Given a list of cells, return a list with 
all of the cells that are alive in that list
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param list a list of cells 
@param w width of the grid
@param h height of the grid
@param tree a tree with coordinate objects at its nodes. the
coordinate objects represent the position of a live cell
in the grid.
@return A list of all the alive cells from the given list
|#
(defun aliveMembers (list tree)
  (if (listp list)
      (if (not(null list))
          (if (avl-retrieve tree (car list))
              (cons (car list) (aliveMembers (cdr list) tree))
              (aliveMembers (cdr list) tree))
          nil)
      nil))

#|
Given a cell, return a list with all the neighbors of that
cell that are alive.
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param cell coodinate structure of the cell from which we 
want to get the neighbor
@param w width of the grid
@param h height of the grid
@param tree a tree with coordinate objects at its nodes. the
coordinate objects represent the position of a live cell
in the grid.
@return A list of all the alive neighbors of a cell
|#
(defun aliveNeighbors (topology cell w h tree)
  (aliveMembers (getNeighbors topology cell w h) tree))

#|
Counts the number of neighbors that are alive given a cell.
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param cell coodinate structure of the cell from which we 
want to get the neighbor
@param w width of the grid
@param h height of the grid
@param tree a tree with coordinate objects at its nodes. the
coordinate objects represent the position of a live cell
in the grid.
@return Number of alive neighbors
|#
(defun numNeighborsAlive (cell topology w h tree)
  (length (aliveNeighbors topology cell w h tree)))

#|
Creates a list of neighbors.
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param list A list of cells
@param w width of the grid
@param h height of the grid
@param tree a tree with coordinate objects at its nodes. the
coordinate objects represent the position of a live cell
in the grid.
@return A list with all the neighbors of the cells of the
given list
|#
(defun allNeighbors (list topology w h)
  (if (consp list)
      (concatenate 'list (getNeighbors topology (car list) w h)
             (allNeighbors (cdr list) topology w h))
      nil))

#|
Creates a list of all the cells for which it needs to be 
determine existance in the world next step.
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param w width of the grid
@param h height of the grid
@param tree a tree with coordinate objects at its nodes. the
coordinate objects represent the position of a live cell
in the grid.
@return A list of all cells for checking
|#
(defun getNodesToCheck (tree topology w h)
  (concatenate 'list (flatTree (avl-flatten tree))
         (allNeighbors (flatTree (avl-flatten tree)) topology w h)))



#|
Given a cell, it determines if it should be alive next round.
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param cell coodinate structure of the cell from which we 
want to get the neighbor.
@param w width of the grid.
@param h height of the grid.
@param tree a tree with coordinate objects at its nodes. the
coordinate objects represent the position of a live cell
in the grid.
@return true or false depending on wether a cell will be alive
next round.
|#
(defun isAliveNextRound (cell tree topology w h)
  (let* ((numAlive (numNeighborsAlive cell topology w h tree)))
    (if (or (and (avl-retrieve tree cell)
                 (= numAlive 2))
            (= numAlive 3))
        t
        nil)))

#|
Given a list of cells, it creates a list with all of the
cells that willl be alive next round from the given list.
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param list A list of cells.
@param w width of the grid.
@param h height of the grid.
@param tree a tree with coordinate objects at its nodes. the
coordinate objects represent the position of a live cell
in the grid.
@return A list of cells.
|#
(defun allAliveNextRound (list tree topology w h)
  (if (and (listp list)(not(null list)))
      (if (isAliveNextRound (car list) tree topology w h)
          (cons (car list) (allAliveNextRound (cdr list) tree topology w h))
          (allAliveNextRound (cdr list) tree topology w h))
      nil))

#|
Given a list, It creates a tree from the cells in the list.
@param topology a symbol that determines the topology of the
grid ('rectangle, 'torus, etc.)
@param list A list of cells
@return A tree.
|#
(defun putInTree (list)
  (if (consp list)
      (avl-insert (putInTree (cdr list)) (car list) t)
      (empty-tree)))

#|
 This is the world structure that contains the major components
 of each world. These are the tree structure, the height, 
 width, the topology displayed, and the cursor. The flag determines if
 the simulation is currently running or not. 
|#
(defstructure theWorld
  (cellsAlive (:assert (tree? cellsAlive)))
  (gridHeight (:assert (natp gridHeight)))
  (gridWidth (:assert (natp gridWidth)))
  (topology (:assert (symbolp topology)))
  (cursor (:assert (isCoord cursor)))
  (flag (:assert (natp flag)))
  (viewportOrigin (:assert (isCoord viewportOrigin))))


(defconst *initial-world* 
  (theWorld nil 10 10 'regular (Coord 0 0) 0 (Coord 0 0)))


#|
Given a world, It creates what the world in the next step 
should be.
@param world A world structure.
@return A world structure.
|#
(defun gerardosNextWorld (world)
  (let* ((toCheck (removeDups (getNodesToCheck (theWorld-cellsAlive world)
                                   (theWorld-topology world)
                                   (theWorld-gridWidth world)
                                   (theWorld-gridHeight world)))))
    (theWorld 
     (putInTree (allAliveNextRound toCheck 
                                   (theWorld-cellsAlive world)
                                   (theWorld-topology world)
                                   (theWorld-gridWidth world)
                                   (theWorld-gridHeight world)))
     (theWorld-gridHeight world)
     (theWorld-gridWidth world)
     (theWorld-topology world)
     (theWorld-cursor world)
     (theWorld-flag world)
     (theWorld-viewportOrigin world))))


  

(defconst *SQUARE* 30)
(defconst *GRIDX* 360)
(defconst *GRIDY* 30)  


;;(include-book "arithmetic/top" :dir :system)

(defun drawGridHelper (scene w1 h1 w2 h2)
      (if (and (natp w2) (>= w2 1))
          (let* ((newImage (add-line scene (+ *GRIDX* (* *SQUARE* (- w2 1))) 
                                     *GRIDY* (+ *GRIDX* (* *SQUARE* (- w2 1)))

                                     (+ *GRIDY* (* *SQUARE* h1)) 'black)) 
                 (newImage2 (add-line newImage (+ *GRIDX* (* *SQUARE* w1))
                                      (+ *GRIDY* (* *SQUARE* h2)) *GRIDX* 
                                      (+ *GRIDY* (* *SQUARE* h2)) 'black))) 
            (drawGridHelper newImage2 w1 h1 (- w2 1) (- h2 1)))
          scene)) 
            
(defun drawGrid(scene w h)

  (drawGridHelper scene w h (+ w 1) h))


#|
 This function draws the actual cursor in the grid. It takes a scene, and a list
 of squares. It is called by 
|#
(defun drawCursor (scene cursor)
  (place-image (rectangle *SQUARE* *SQUARE* 'solid 'blue) (+ *GRIDX* (* (Coord-cellX cursor) *SQUARE*)) (+ *GRIDY* (* (Coord-cellY cursor) *SQUARE*)) scene))  

  
#|
 These are constants that define the offsets for the instructional text placement.
|#
(defconst *XINIT*  10)
(defconst *XOFFSET* 90)
(defconst *YINIT* 10)
(defconst *INC* 20)

#|
 These are constants used for the flag to determine if the simulation is running or not.
|#
(defconst *RUNNING* 1)

#|
 This function displays the instructional text that guides the user. It is called
 in makeGUI and takes in a scene. 
|#
(defun instructionText (scene w)
  (place-image (text "TEAM TURING" 16 'red) *XINIT* (+ *YINIT* (* *INC* 1))
  (place-image (text "Conway's Game of Life" 14 'blue) *XINIT* (+ *YINIT* (* *INC* 3))  
  (place-image (text "Choose starting cells using your arrow keys." 11 'black) *XINIT* (+ *YINIT* (* *INC* 5))
  (place-image (text "Press 'a' to activate or deactivate cells." 11 'black) *XINIT* (+ *YINIT* (* *INC* 6))
  (place-image (text "Pick a size:"  11 'black) *XINIT* (+ *YINIT* (* *INC* 8))
  (place-image (text "Press '1' for 10x10 size grid" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 9))             
  (place-image (text "Press '5' for 15x15 size grid" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 10)) 
  (place-image (text "Press '2' for 20x20 size grid" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 11)) 
  (place-image (text "Pick a topology:" 11 'black) *XINIT* (+ *YINIT* (* *INC* 13))
  (place-image (text "Press 'k' for klein bottle" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 14))
  (place-image (text "Press 't' for torus" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 15))
  (place-image (text "Press 'c' for cylinder" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 16))
  (place-image (text "Press 'm' for mobius strip" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 17))
  (place-image (text "Press 'r' for regular" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 18))
  (place-image (text "Press 'h' for infinite hex" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 19))
  (place-image (text "Panning infinite hex grid" 11 'black) *XINIT* (+ *YINIT* (* *INC* 21))
  (place-image (text "Press v (left)" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 22)) 
  (place-image (text "Press b (down)" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 23)) 
  (place-image (text "Press n (right)" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 24)) 
  (place-image (text "Press g (up)" 11 'black) *XOFFSET* (+ *YINIT* (* *INC* 25)) 
  (place-image (text "Your current topology:  " 11 'black) *XINIT* (+ *YINIT* (* *INC* 27)) 
  (place-image (text (string (theWorld-topology w)) 11 'green) *XOFFSET* (+ *YINIT* (* *INC* 28)) 
  (place-image (text "Press 's' to begin and end the simulation." 11 'blue) *XINIT* (+ *YINIT* (* *INC* 30)) 
  (place-image (text "Press 'p' if you only wnat to go one step." 11 'blue) *XINIT* (+ *YINIT* (* *INC* 31)) 
               
  (place-image (text (if (equal (theWorld-flag w) *RUNNING*)
                         "RUNNING"
                         "NOT RUNNING") 11 'red) *XINIT* (+ *YINIT* (* *INC* 33)) 
   scene))))))))))))))))))))))))))


(defun drawTree (thirdImage currentTree width height originx originy)
  (if (and (tree? currentTree)(consp currentTree))
      (let* ((root (key currentTree))

         (xCoord (car root))
         (yCoord (cdr root))
         (image (if (empty-tree? currentTree)
              thirdImage
              (if (and (> (+ originx width) xCoord)
                       (> (+ originy height) yCoord)
                       (<= originy yCoord)
                       (<= originx xCoord))
                  (place-image (rectangle *SQUARE* *SQUARE* 'solid 'red) 
                               (+ *GRIDX* (* (- xCoord originx) *SQUARE*)) (+ *GRIDY* (* (- yCoord originy) *SQUARE*)) thirdImage)
                  thirdImage)))
         (imageTwo (if (empty-tree? (left currentTree))
                       image
                       (drawTree image (left currentTree) width height originx originy))))
         (if (empty-tree? (right currentTree))
             imageTwo
             (drawTree imageTwo (right currentTree) width height originx originy))) 
      thirdImage))


(defun checkFlag (w)
  (if (equal (theWorld-flag w) *RUNNING*)
        (gerardosNextWorld w)
        w))


#|
 This function is called by world-image. It receives the scene
 and world. It sets the world components and calls drawGrid to
 draw the grid initially. 
|#
(defun makeGUI (w image)
  (let* ((width (theWorld-gridWidth w))
        (height (theWorld-gridHeight w))
        (currentTree (theWorld-cellsAlive w))
        (cursor (theWorld-cursor w))
        (firstImage (instructionText image w))
        (secondImage (drawGrid firstImage width height))
        (thirdImage  (drawCursor secondImage cursor)))
      (drawTree thirdImage currentTree (theWorld-gridWidth w) (theWorld-gridHeight w) (Coord-cellX (theWorld-viewportOrigin w)) (Coord-cellY (theWorld-viewportOrigin w)))))

#|
 Produces an image of the given world. *WIDTH* AND *HEIGHT*
 are constants stated in the beginning of this file. They
 define the size of the GUI window. 
|#
(defun world-image (w)
  (makeGui w (empty-scene *WIDTH* *HEIGHT*)))


#|
 This function is called on a key press event. I takes
 in the world and the key that was preseed and checks to
 see which key was pressed. Depending on the key, the appropriate
 action is taken and the world is passed on. 
|# 
(defun handleKeyPress (w key)
      (let* ((topo (cond ((eql #\k key) 'klein)
                     ((eql #\t key) 'torus)
                     ((eql #\m key) 'mobius)
                     ((eql #\c key) 'cylinder)
                     ((eql #\r key) 'regular)
                     ((eql #\h key) 'infiniteHex!)
                     (t (theWorld-topology w))))
         (wh (cond ((equal #\2 key) (list 20 20))
                   ((equal #\5 key) (list 15 15))
                   ((equal #\1 key) (list 10 10))
                   (t (list (theWorld-gridWidth w) (theWorld-gridHeight w)))))
         (cursorx (Coord-cellX (theWorld-cursor w)))
         (cursory (Coord-cellY (theWorld-cursor w)))
         (currentTree (theWorld-cellsAlive w))
         (above (aboveNeighbor (theWorld-topology w) (Coord cursorx cursory) (theWorld-gridHeight w)))
         (below (belowNeighbor (theWorld-topology w) (Coord cursorx cursory) (theWorld-gridHeight w)))
         (left (leftNeighbor (theWorld-topology w) (Coord cursorx cursory) (theWorld-gridHeight w)))
         (right (rightNeighbor (theWorld-topology w) (Coord cursorx cursory) (theWorld-gridHeight w)))
         (c (cond ((equal 'up key) (if above above (theWorld-cursor w)))
                  ((equal 'down key) (if below below (theWorld-cursor w)))
                  ((equal 'left key) (if left left (theWorld-cursor w)))
                  ((equal 'right key) (if right right (theWorld-cursor w)))
                  (t (theWorld-cursor w))))
         (tree (if (equal #\a key) (if (avl-retrieve currentTree (Coord cursorx cursory))
                                       (avl-delete currentTree (Coord cursorx cursory))
                                       (avl-insert currentTree (Coord cursorx cursory) t))
                   currentTree))
         (flag (if (equal #\s key)
                   (if (equal *RUNNING* (theWorld-flag w))
                       (not *RUNNING*)
                       *RUNNING*)
                   (theWorld-flag w)))
         (viewportOrigin (cond ((eql #\g key) (Coord (Coord-cellX (theWorld-viewportOrigin w)) (- (Coord-cellY (theWorld-viewportOrigin w)) 1)))
                               ((eql #\v key) (Coord (- (Coord-cellX (theWorld-viewportOrigin w)) 1) (Coord-cellY (theWorld-viewportOrigin w))))
                               ((eql #\b key) (Coord (Coord-cellX (theWorld-viewportOrigin w)) (+ (Coord-cellY (theWorld-viewportOrigin w)) 1)))
                               ((eql #\n key) (Coord (+ (Coord-cellX (theWorld-viewportOrigin w)) 1) (Coord-cellY (theWorld-viewportOrigin w))))
                               (t (theWorld-viewportOrigin w)))))
    (if (equal #\p key)
        (gerardosNextWorld w)
        (theWorld tree (car wh) (car(cdr wh)) topo c flag viewportOrigin))))
                  
;#|
;Now we get the ball rolling by calling big-bang.  It consumes the width and
;height of the playing field, a number indicating how often the clock ticks, and
;the initial world.  In this case, the clock ticks every 1/10 second.
;|#

(big-bang *WIDTH* *HEIGHT* 1/10 *initial-world*)

;;; Every time the world changes, the it must be redrawn.  We provide
;;; on-redraw with the function that produces an image given a world.
(on-redraw world-image)
;
;;; At each clock tick, the worm must move a step in the direction it faces.
;;; on-tick-event consumes the function that takes the world and produces the
;;; next world. Checks the current status of the flag (simulation running or not)
(on-tick-event checkFlag)



;;; When a key is pressed, the world changes (the arrow keys change the
;;; direction of the worm, for example).  on-key-event consumes the function
;;; that produces a new world given the current world and a keyboard input.
(on-key-event handleKeyPress)


#| Theorem that proves that if a cell is a coordinate
   than it consists of an x and y value.
|#
(defthm cell-consists-of-x-and-y
  (implies (isCoord cell)
           (= (Coord (Coord-cellX cell) (Coord-cellY cell)) cell)))

#| Theorem that proves that if a cell is a coordinate
   than it will have a left neighbor.
|#
(defthm cell-left-neighbor
  (implies (and (isCoord cell)
                (symbolp topology)
                (natp w))
           (leftNeighbor topology cell w)))

#| Theorem that proves that if a cell is a coordinate
   than it will have a right neighbor
|#
(defthm cell-right-neighbor
  (implies (and (isCoord cell)
                (symbolp topology)
                (natp w))
           (rightNeighbor topology cell w)))


#| Induction hint |#
(defun hint-neighbor-induct(w y)
  (if (and (natp y) (>= y 1))
      (hint-neighbor-induct w (- y 1))
      (cons w y)))

#| Theorem that proves that in the torus topology
   the furthest right cell's neighbor will be equal to the
   first cell in that saw row and that the furthest left cell's
   neighbor will be the last cell in that same row.
|#
(defthm torus-side-wrap-around-neighbor
  (implies (and (natp w)
                (natp y)
                (>= y 0))
           (and(= (Coord 0 y) (rightNeighbor 'torus 
                                             (Coord w y) (+ w 1)))
               (= (Coord w y) (leftNeighbor 'torus 
                                            (Coord 0 y) (+ w 1)))))
  :hints(("Goal":induct(hint-neighbor-induct w y))))


#| Theorem that proves that in the torus topology
   the furthest top cell's above neighbor will be equal to the
   bottom cell in that saw column and that the furthest bottom cell's
   below neighbor will be the a cell in the top row that is in the 
   same colummn.
|#
(defthm torus-top-wrap-around-neighbor
  (implies (and (natp w)
                (natp x)
                (>= x 0)
                (> (- w w) 0))
           (and(= (Coord x w) (aboveNeighbor 'torus 
                                             (Coord x 0) (+ w 1)))
               (= (Coord x 0) (belowNeighbor 'torus 
                                            (Coord x w) (+ w 1)))))
  :hints(("Goal":induct(hint-neighbor-induct w x))))

#| Theorem that proves that in the klein bottle topology
   any cell in the top row will have an above neighbor in the
   bottom row, but shifted as dictated by the topology. Similarily,
   any cell in the bottom row will have a below neighbor in 
   the top row but shifted as dictated by the topology.
|#
(defthm klein-bottle-top-bottom-wrap-around
  (implies (and (natp w)
                (natp y)
                (natp x)
                (> ( - w w) 0))
            (and (= (Coord x w) (aboveNeighbor 'klein 
                                               (Coord w 0) (+ w 1)))
                 (= (Coord 0 y) (belowNeighbor 'klein 
                                               (Coord w w) (+ w 1)))))
   :hints (("Goal":induct(hint-neighbor-induct w x)))) 

#| Theorem that proves that in the mobius strip topology
   any cell in the top row will have an above neighbor in
   bottom row but shifted as dictated by the topology. Similarly, 
   any cell in the bottom row will have a below neighbor in 
   the top row but shifted as dictated by the topology.
|#
(defthm mobius-strip-top-bottom-wrap-around
  (implies (and (natp w)
                (natp y)
                (natp x)
                (> ( - w w) 0))
            (and (= (Coord x w) (aboveNeighbor 'mobius 
                                               (Coord w 0) (+ w 1)))
                 (= (Coord 0 y) (belowNeighbor 'mobius 
                                               (Coord w w) (+ w 1)))))
   :hints (("Goal":induct(hint-neighbor-induct w y)))) 


#| Theorem that proves that in the rectangle topology
   a given cell will have a left neighbor that's x value
   is the difference of 1 from the given cell's x value, a
   right neighbor that's x value will be 1 more than the
   given cell's x value, an above neighbor whose y value is 
   one less than the given cell's y value, and a below 
   neighbor whose y value is 1 more than the given cell's
   y value.
|#
(defthm rectangle-neighbors
  (implies (and (natp x)
                (natp y)
                (natp w)
                (<= x w)
                (<= y w)
                (> (- w w) 0))
           (and (= (Coord (+ x 1) y)
                   (rightNeighbor 'rectangle (Coord x y) (+ w 1)))
                (= (Coord (- x 1) y)
                   (leftNeighbor 'rectangle (Coord x y) (+ w 1)))
                (= (Coord x (- y 1))
                   (aboveNeighbor 'rectangle (Coord x y) (+ w 1)))
                (= (Coord x (+ y 1))
                   (belowNeighbor 'rectangle (Coord x y) (+ w 1)))))
   :hints (("Goal":induct(hint-neighbor-induct w y))))






























































































































































